D:Dsys, v:(i:IdM(i).(timed)state), sched:(Id(?((IdLnk + Id)))),
dec:(i,a:IdM(i).state(?if a  dom(M(i).prob) then Outcome else Void fi )),
discrete:(IdId).
Feasible(D)  (d-world(D;v;sched;dec;discrete)  World) 

latex

Definitions

Top, x:A  B(x), , x:A. B(x), locl(a), M(i), M.da(a), x.A(x), M.ds(x), M.dout(l,tg), w-automaton(T;TA;M), mlnk(m), source(l), Msg(M), {x:A| B(x)} , type List, w-action-dec(TA;M;i), Action(dec), <a, b>, M.(timed)state, t.1, f(x)?z, f(a), P  Q, False, A, A  B, , CV(F), , S  T, suptype(S; T), M.init(x)?v, (i = j), if b then t else f fi , IdLnk, d-world(D;v;sched;dec;discrete), World, Dsys, Unit, left + right, ma-prob(M;b), Outcome, b  dom(M.prob), M.state, Feasible(D), Type, Void, t  T, d-comp(D; v; sched; dec; d), d-world-state(D;i), Id, x:AB(x), #$n, {i..j}, , s = t, b, , b, P & Q, P  Q, timedState(ds), n - m, -n, n+m, a < b, Knd, t.2, rcv(l,tg), Msg(da), M.Msg, d-decl(D;i), x:A.B(x), , d-machine(i;M;dec)

Lemmas

d-machine wf, it wf, subtype rel list, ma-msg wf, mlnk wf d, subtype rel self, CV wf, le wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, bnot wf, not wf, assert wf, d-feasible wf, bool wf, ma-st wf, ma-prob-dom wf, p-outcome wf, ma-prob wf, unit wf, ma-tst wf, dsys wf, d-comp wf2, int seg wf, d-world-state wf, Id wf, ma-dout wf, IdLnk wf, ifthenelse wf, eq int wf, ma-init-val wf, rationals wf, nat wf, action wf, w-action-dec wf, Msg wf, lsrc wf, mlnk wf, w-automaton wf, ma-ds wf, d-m wf, ma-da wf, locl wf, top wf